WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3)))
cond_eval_expr_1(Zero(),x3) -> eval#1(x3)
cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10)
cond_eval_expr_2(Zero(),x2) -> eval#1(x2)
cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5)))
cond_eval_expr_3(Zero(),x5) -> Zero()
eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12)
eval#1(Nat(x4)) -> x4
eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8)
main(x0) -> eval#1(x0)
- Signature:
{cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1} / {Add/2,Nat/1,Sub/2,Succ/1
,Zero/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_eval_expr_1,cond_eval_expr_2,cond_eval_expr_3,eval#1
,main} and constructors {Add,Nat,Sub,Succ,Zero}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
cond_eval_expr_3#(Zero(),x5) -> c_6()
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Nat(x4)) -> c_8()
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
main#(x0) -> c_10(eval#1#(x0))
Weak DPs
and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
cond_eval_expr_3#(Zero(),x5) -> c_6()
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Nat(x4)) -> c_8()
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
main#(x0) -> c_10(eval#1#(x0))
- Weak TRS:
cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3)))
cond_eval_expr_1(Zero(),x3) -> eval#1(x3)
cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10)
cond_eval_expr_2(Zero(),x2) -> eval#1(x2)
cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5)))
cond_eval_expr_3(Zero(),x5) -> Zero()
eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12)
eval#1(Nat(x4)) -> x4
eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8)
main(x0) -> eval#1(x0)
- Signature:
{cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2
,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1
,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#
,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{6,8}
by application of
Pre({6,8}) = {2,3,4,7,9,10}.
Here rules are labelled as follows:
1: cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
2: cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
3: cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
4: cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
5: cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
6: cond_eval_expr_3#(Zero(),x5) -> c_6()
7: eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
8: eval#1#(Nat(x4)) -> c_8()
9: eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
10: main#(x0) -> c_10(eval#1#(x0))
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
main#(x0) -> c_10(eval#1#(x0))
- Weak DPs:
cond_eval_expr_3#(Zero(),x5) -> c_6()
eval#1#(Nat(x4)) -> c_8()
- Weak TRS:
cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3)))
cond_eval_expr_1(Zero(),x3) -> eval#1(x3)
cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10)
cond_eval_expr_2(Zero(),x2) -> eval#1(x2)
cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5)))
cond_eval_expr_3(Zero(),x5) -> Zero()
eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12)
eval#1(Nat(x4)) -> x4
eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8)
main(x0) -> eval#1(x0)
- Signature:
{cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2
,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1
,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#
,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
-->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
2:S:cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
-->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
-->_1 eval#1#(Nat(x4)) -> c_8():10
3:S:cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
-->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
-->_1 cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))):5
-->_2 eval#1#(Nat(x4)) -> c_8():10
-->_1 cond_eval_expr_3#(Zero(),x5) -> c_6():9
4:S:cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
-->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
-->_1 eval#1#(Nat(x4)) -> c_8():10
5:S:cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
-->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
6:S:eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
-->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_2 eval#1#(Nat(x4)) -> c_8():10
-->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
-->_1 cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)):2
-->_1 cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))):1
7:S:eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
-->_2 eval#1#(Nat(x4)) -> c_8():10
-->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
-->_1 cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)):4
-->_1 cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)):3
8:S:main#(x0) -> c_10(eval#1#(x0))
-->_1 eval#1#(Nat(x4)) -> c_8():10
-->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
9:W:cond_eval_expr_3#(Zero(),x5) -> c_6()
10:W:eval#1#(Nat(x4)) -> c_8()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
9: cond_eval_expr_3#(Zero(),x5) -> c_6()
10: eval#1#(Nat(x4)) -> c_8()
* Step 4: RemoveHeads WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
main#(x0) -> c_10(eval#1#(x0))
- Weak TRS:
cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3)))
cond_eval_expr_1(Zero(),x3) -> eval#1(x3)
cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10)
cond_eval_expr_2(Zero(),x2) -> eval#1(x2)
cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5)))
cond_eval_expr_3(Zero(),x5) -> Zero()
eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12)
eval#1(Nat(x4)) -> x4
eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8)
main(x0) -> eval#1(x0)
- Signature:
{cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2
,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1
,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#
,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero}
+ Applied Processor:
RemoveHeads
+ Details:
Consider the dependency graph
1:S:cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
-->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
2:S:cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
-->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
3:S:cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
-->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
-->_1 cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5)))):5
4:S:cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
-->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
5:S:cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
-->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
6:S:eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
-->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
-->_1 cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3)):2
-->_1 cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3))):1
7:S:eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
-->_2 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_2 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
-->_1 cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2)):4
-->_1 cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5)):3
8:S:main#(x0) -> c_10(eval#1#(x0))
-->_1 eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14)):7
-->_1 eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10)):6
Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
[(8,main#(x0) -> c_10(eval#1#(x0)))]
* Step 5: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
- Weak TRS:
cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3)))
cond_eval_expr_1(Zero(),x3) -> eval#1(x3)
cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10)
cond_eval_expr_2(Zero(),x2) -> eval#1(x2)
cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5)))
cond_eval_expr_3(Zero(),x5) -> Zero()
eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12)
eval#1(Nat(x4)) -> x4
eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8)
main(x0) -> eval#1(x0)
- Signature:
{cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2
,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1
,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#
,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3)))
cond_eval_expr_1(Zero(),x3) -> eval#1(x3)
cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10)
cond_eval_expr_2(Zero(),x2) -> eval#1(x2)
cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5)))
cond_eval_expr_3(Zero(),x5) -> Zero()
eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12)
eval#1(Nat(x4)) -> x4
eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8)
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
* Step 6: Ara WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
- Weak TRS:
cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3)))
cond_eval_expr_1(Zero(),x3) -> eval#1(x3)
cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10)
cond_eval_expr_2(Zero(),x2) -> eval#1(x2)
cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5)))
cond_eval_expr_3(Zero(),x5) -> Zero()
eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12)
eval#1(Nat(x4)) -> x4
eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8)
- Signature:
{cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2
,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1
,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#
,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
Add :: ["A"(4) x "A"(4)] -(0)-> "A"(4)
Add :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
Nat :: ["A"(0)] -(0)-> "A"(0)
Nat :: ["A"(0)] -(0)-> "A"(13)
Nat :: ["A"(0)] -(0)-> "A"(14)
Nat :: ["A"(0)] -(0)-> "A"(10)
Nat :: ["A"(0)] -(0)-> "A"(15)
Nat :: ["A"(0)] -(0)-> "A"(7)
Sub :: ["A"(4) x "A"(4)] -(4)-> "A"(4)
Sub :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
Succ :: ["A"(0)] -(0)-> "A"(0)
Succ :: ["A"(0)] -(0)-> "A"(3)
Zero :: [] -(0)-> "A"(0)
Zero :: [] -(0)-> "A"(7)
cond_eval_expr_1 :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
cond_eval_expr_2 :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
cond_eval_expr_3 :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
eval#1 :: ["A"(0)] -(0)-> "A"(0)
cond_eval_expr_1# :: ["A"(0) x "A"(4)] -(0)-> "A"(0)
cond_eval_expr_2# :: ["A"(0) x "A"(4)] -(4)-> "A"(8)
cond_eval_expr_3# :: ["A"(0) x "A"(0)] -(4)-> "A"(13)
eval#1# :: ["A"(4)] -(0)-> "A"(1)
c_1 :: ["A"(1)] -(0)-> "A"(1)
c_2 :: ["A"(0)] -(0)-> "A"(12)
c_3 :: ["A"(0) x "A"(0)] -(0)-> "A"(12)
c_4 :: ["A"(0)] -(0)-> "A"(12)
c_5 :: ["A"(0)] -(0)-> "A"(15)
c_7 :: ["A"(0) x "A"(0)] -(0)-> "A"(12)
c_9 :: ["A"(1) x "A"(0)] -(0)-> "A"(1)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"Add_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
"Nat_A" :: ["A"(0)] -(0)-> "A"(1)
"Sub_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
"Succ_A" :: ["A"(0)] -(0)-> "A"(1)
"Zero_A" :: [] -(0)-> "A"(1)
"c_1_A" :: ["A"(0)] -(0)-> "A"(1)
"c_2_A" :: ["A"(0)] -(0)-> "A"(1)
"c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
"c_4_A" :: ["A"(0)] -(0)-> "A"(1)
"c_5_A" :: ["A"(0)] -(0)-> "A"(1)
"c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
"c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
2. Weak:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
* Step 7: Ara WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
- Weak DPs:
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
- Weak TRS:
cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3)))
cond_eval_expr_1(Zero(),x3) -> eval#1(x3)
cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10)
cond_eval_expr_2(Zero(),x2) -> eval#1(x2)
cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5)))
cond_eval_expr_3(Zero(),x5) -> Zero()
eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12)
eval#1(Nat(x4)) -> x4
eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8)
- Signature:
{cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2
,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1
,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#
,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
Add :: ["A"(2) x "A"(2)] -(2)-> "A"(2)
Add :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
Nat :: ["A"(0)] -(0)-> "A"(0)
Nat :: ["A"(0)] -(0)-> "A"(12)
Nat :: ["A"(0)] -(0)-> "A"(14)
Nat :: ["A"(0)] -(0)-> "A"(10)
Nat :: ["A"(0)] -(0)-> "A"(2)
Nat :: ["A"(0)] -(0)-> "A"(8)
Nat :: ["A"(0)] -(0)-> "A"(4)
Sub :: ["A"(2) x "A"(2)] -(0)-> "A"(2)
Sub :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
Sub :: ["A"(8) x "A"(8)] -(0)-> "A"(8)
Succ :: ["A"(0)] -(0)-> "A"(0)
Succ :: ["A"(0)] -(0)-> "A"(2)
Zero :: [] -(0)-> "A"(0)
Zero :: [] -(0)-> "A"(15)
cond_eval_expr_1 :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
cond_eval_expr_2 :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
cond_eval_expr_3 :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
eval#1 :: ["A"(0)] -(0)-> "A"(0)
cond_eval_expr_1# :: ["A"(0) x "A"(2)] -(2)-> "A"(2)
cond_eval_expr_2# :: ["A"(0) x "A"(2)] -(0)-> "A"(1)
cond_eval_expr_3# :: ["A"(0) x "A"(0)] -(0)-> "A"(9)
eval#1# :: ["A"(2)] -(0)-> "A"(12)
c_1 :: ["A"(0)] -(0)-> "A"(10)
c_2 :: ["A"(0)] -(0)-> "A"(10)
c_3 :: ["A"(0) x "A"(1)] -(0)-> "A"(1)
c_4 :: ["A"(0)] -(0)-> "A"(4)
c_5 :: ["A"(0)] -(0)-> "A"(14)
c_7 :: ["A"(0) x "A"(0)] -(0)-> "A"(14)
c_9 :: ["A"(0) x "A"(0)] -(0)-> "A"(12)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"Add_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
"Nat_A" :: ["A"(0)] -(0)-> "A"(1)
"Sub_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1)
"Succ_A" :: ["A"(0)] -(0)-> "A"(1)
"Zero_A" :: [] -(0)-> "A"(1)
"c_1_A" :: ["A"(0)] -(0)-> "A"(1)
"c_2_A" :: ["A"(0)] -(0)-> "A"(1)
"c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
"c_4_A" :: ["A"(0)] -(0)-> "A"(1)
"c_5_A" :: ["A"(0)] -(0)-> "A"(1)
"c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
"c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
2. Weak:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
* Step 8: Ara WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
- Weak DPs:
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
- Weak TRS:
cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3)))
cond_eval_expr_1(Zero(),x3) -> eval#1(x3)
cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10)
cond_eval_expr_2(Zero(),x2) -> eval#1(x2)
cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5)))
cond_eval_expr_3(Zero(),x5) -> Zero()
eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12)
eval#1(Nat(x4)) -> x4
eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8)
- Signature:
{cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2
,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1
,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#
,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
Add :: ["A"(8, 8) x "A"(8, 8)] -(0)-> "A"(0, 8)
Add :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0)
Nat :: ["A"(8, 0)] -(0)-> "A"(8, 0)
Nat :: ["A"(8, 0)] -(0)-> "A"(8, 14)
Nat :: ["A"(8, 0)] -(0)-> "A"(8, 8)
Nat :: ["A"(8, 0)] -(0)-> "A"(8, 3)
Nat :: ["A"(8, 0)] -(0)-> "A"(8, 1)
Sub :: ["A"(8, 8) x "A"(8, 8)] -(0)-> "A"(0, 8)
Sub :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0)
Succ :: ["A"(8, 0)] -(8)-> "A"(8, 0)
Succ :: ["A"(8, 0)] -(8)-> "A"(8, 10)
Zero :: [] -(0)-> "A"(8, 0)
Zero :: [] -(0)-> "A"(8, 8)
cond_eval_expr_1 :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0)
cond_eval_expr_2 :: ["A"(8, 0) x "A"(8, 0)] -(0)-> "A"(8, 0)
cond_eval_expr_3 :: ["A"(8, 0) x "A"(8, 0)] -(8)-> "A"(8, 0)
eval#1 :: ["A"(8, 0)] -(0)-> "A"(8, 0)
cond_eval_expr_1# :: ["A"(8, 0) x "A"(8, 8)] -(0)-> "A"(2, 0)
cond_eval_expr_2# :: ["A"(8, 0) x "A"(8, 8)] -(0)-> "A"(1, 4)
cond_eval_expr_3# :: ["A"(8, 0) x "A"(8, 0)] -(4)-> "A"(1, 0)
eval#1# :: ["A"(0, 8)] -(0)-> "A"(4, 0)
c_1 :: ["A"(0, 0)] -(0)-> "A"(4, 12)
c_2 :: ["A"(0, 0)] -(0)-> "A"(3, 0)
c_3 :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 6)
c_4 :: ["A"(0, 0)] -(0)-> "A"(12, 14)
c_5 :: ["A"(0, 0)] -(0)-> "A"(1, 0)
c_7 :: ["A"(2, 0) x "A"(2, 0)] -(0)-> "A"(4, 2)
c_9 :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(8, 6)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"Add_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
"Add_A" :: ["A"(1, 1) x "A"(1, 1)] -(0)-> "A"(0, 1)
"Nat_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0)
"Nat_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1)
"Sub_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
"Sub_A" :: ["A"(1, 1) x "A"(1, 1)] -(0)-> "A"(0, 1)
"Succ_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0)
"Succ_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1)
"Zero_A" :: [] -(0)-> "A"(1, 0)
"Zero_A" :: [] -(0)-> "A"(0, 1)
"c_1_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_1_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_2_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_2_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
"c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1)
"c_4_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_4_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_5_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_5_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
"c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1)
"c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
"c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
2. Weak:
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
* Step 9: Ara WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
- Weak DPs:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
- Weak TRS:
cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3)))
cond_eval_expr_1(Zero(),x3) -> eval#1(x3)
cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10)
cond_eval_expr_2(Zero(),x2) -> eval#1(x2)
cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5)))
cond_eval_expr_3(Zero(),x5) -> Zero()
eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12)
eval#1(Nat(x4)) -> x4
eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8)
- Signature:
{cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2
,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1
,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#
,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
Add :: ["A"(11, 11) x "A"(0, 11)] -(11)-> "A"(0, 11)
Add :: ["A"(11, 0) x "A"(11, 0)] -(0)-> "A"(11, 0)
Nat :: ["A"(11, 0)] -(0)-> "A"(11, 0)
Nat :: ["A"(11, 0)] -(0)-> "A"(11, 14)
Nat :: ["A"(11, 0)] -(0)-> "A"(11, 1)
Nat :: ["A"(11, 0)] -(0)-> "A"(11, 12)
Nat :: ["A"(11, 0)] -(0)-> "A"(11, 11)
Sub :: ["A"(11, 11) x "A"(11, 11)] -(11)-> "A"(0, 11)
Sub :: ["A"(11, 0) x "A"(11, 0)] -(11)-> "A"(11, 0)
Succ :: ["A"(11, 0)] -(11)-> "A"(11, 0)
Succ :: ["A"(11, 0)] -(11)-> "A"(11, 6)
Zero :: [] -(0)-> "A"(11, 0)
Zero :: [] -(0)-> "A"(11, 8)
cond_eval_expr_1 :: ["A"(11, 0) x "A"(11, 0)] -(0)-> "A"(11, 0)
cond_eval_expr_2 :: ["A"(11, 0) x "A"(11, 0)] -(0)-> "A"(11, 0)
cond_eval_expr_3 :: ["A"(11, 0) x "A"(11, 0)] -(7)-> "A"(11, 0)
eval#1 :: ["A"(11, 0)] -(0)-> "A"(11, 0)
cond_eval_expr_1# :: ["A"(11, 0) x "A"(0, 11)] -(6)-> "A"(5, 13)
cond_eval_expr_2# :: ["A"(11, 0) x "A"(11, 11)] -(1)-> "A"(4, 4)
cond_eval_expr_3# :: ["A"(11, 0) x "A"(11, 0)] -(4)-> "A"(0, 0)
eval#1# :: ["A"(0, 11)] -(1)-> "A"(14, 0)
c_1 :: ["A"(0, 0)] -(0)-> "A"(7, 15)
c_2 :: ["A"(0, 0)] -(0)-> "A"(5, 14)
c_3 :: ["A"(0, 0) x "A"(10, 0)] -(0)-> "A"(11, 10)
c_4 :: ["A"(0, 0)] -(0)-> "A"(4, 4)
c_5 :: ["A"(0, 0)] -(0)-> "A"(0, 0)
c_7 :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(14, 15)
c_9 :: ["A"(0, 0) x "A"(0, 0)] -(1)-> "A"(14, 1)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"Add_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
"Add_A" :: ["A"(1, 1) x "A"(0, 1)] -(1)-> "A"(0, 1)
"Nat_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0)
"Nat_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1)
"Sub_A" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0)
"Sub_A" :: ["A"(1, 1) x "A"(1, 1)] -(1)-> "A"(0, 1)
"Succ_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0)
"Succ_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1)
"Zero_A" :: [] -(0)-> "A"(1, 0)
"Zero_A" :: [] -(0)-> "A"(0, 1)
"c_1_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_1_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_2_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_2_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
"c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1)
"c_4_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_4_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_5_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_5_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
"c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1)
"c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
"c_9_A" :: ["A"(0) x "A"(0)] -(1)-> "A"(0, 1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
2. Weak:
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
* Step 10: Ara WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
- Weak DPs:
cond_eval_expr_1#(Succ(x5),x3) -> c_1(eval#1#(Add(Nat(x5),x3)))
cond_eval_expr_1#(Zero(),x3) -> c_2(eval#1#(x3))
cond_eval_expr_2#(Zero(),x2) -> c_4(eval#1#(x2))
cond_eval_expr_3#(Succ(x7),x5) -> c_5(eval#1#(Sub(Nat(x7),Nat(x5))))
eval#1#(Sub(x8,x14)) -> c_9(cond_eval_expr_2#(eval#1(x14),x8),eval#1#(x14))
- Weak TRS:
cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3)))
cond_eval_expr_1(Zero(),x3) -> eval#1(x3)
cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10)
cond_eval_expr_2(Zero(),x2) -> eval#1(x2)
cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5)))
cond_eval_expr_3(Zero(),x5) -> Zero()
eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12)
eval#1(Nat(x4)) -> x4
eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8)
- Signature:
{cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1,cond_eval_expr_1#/2
,cond_eval_expr_2#/2,cond_eval_expr_3#/2,eval#1#/1,main#/1} / {Add/2,Nat/1,Sub/2,Succ/1,Zero/0,c_1/1,c_2/1
,c_3/2,c_4/1,c_5/1,c_6/0,c_7/2,c_8/0,c_9/2,c_10/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {cond_eval_expr_1#,cond_eval_expr_2#,cond_eval_expr_3#
,eval#1#,main#} and constructors {Add,Nat,Sub,Succ,Zero}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
Add :: ["A"(3, 3) x "A"(0, 3)] -(3)-> "A"(0, 3)
Add :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(3, 0)
Nat :: ["A"(3, 0)] -(0)-> "A"(3, 0)
Nat :: ["A"(3, 0)] -(0)-> "A"(3, 6)
Nat :: ["A"(3, 0)] -(0)-> "A"(3, 4)
Nat :: ["A"(3, 0)] -(0)-> "A"(3, 2)
Nat :: ["A"(3, 0)] -(0)-> "A"(3, 15)
Nat :: ["A"(3, 0)] -(0)-> "A"(3, 5)
Nat :: ["A"(3, 0)] -(0)-> "A"(3, 14)
Sub :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(3, 0)
Sub :: ["A"(3, 3) x "A"(3, 3)] -(0)-> "A"(0, 3)
Succ :: ["A"(3, 0)] -(3)-> "A"(3, 0)
Zero :: [] -(0)-> "A"(3, 0)
Zero :: [] -(0)-> "A"(11, 8)
cond_eval_expr_1 :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(3, 0)
cond_eval_expr_2 :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(3, 0)
cond_eval_expr_3 :: ["A"(3, 0) x "A"(3, 0)] -(3)-> "A"(3, 0)
eval#1 :: ["A"(3, 0)] -(0)-> "A"(3, 0)
cond_eval_expr_1# :: ["A"(3, 0) x "A"(0, 3)] -(0)-> "A"(1, 3)
cond_eval_expr_2# :: ["A"(3, 0) x "A"(3, 3)] -(0)-> "A"(1, 1)
cond_eval_expr_3# :: ["A"(3, 0) x "A"(3, 0)] -(0)-> "A"(5, 1)
eval#1# :: ["A"(0, 3)] -(0)-> "A"(5, 0)
c_1 :: ["A"(0, 0)] -(0)-> "A"(4, 14)
c_2 :: ["A"(3, 0)] -(0)-> "A"(9, 3)
c_3 :: ["A"(5, 0) x "A"(0, 0)] -(0)-> "A"(3, 2)
c_4 :: ["A"(0, 0)] -(0)-> "A"(14, 9)
c_5 :: ["A"(0, 0)] -(0)-> "A"(12, 4)
c_7 :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(7, 14)
c_9 :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(14, 2)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"Add_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
"Add_A" :: ["A"(1, 1) x "A"(0, 1)] -(1)-> "A"(0, 1)
"Nat_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0)
"Nat_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1)
"Sub_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0)
"Sub_A" :: ["A"(1, 1) x "A"(1, 1)] -(0)-> "A"(0, 1)
"Succ_A" :: ["A"(1, 0)] -(1)-> "A"(1, 0)
"Succ_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1)
"Zero_A" :: [] -(0)-> "A"(1, 0)
"Zero_A" :: [] -(0)-> "A"(0, 1)
"c_1_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_1_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_2_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_2_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
"c_3_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1)
"c_4_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_4_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_5_A" :: ["A"(0)] -(0)-> "A"(1, 0)
"c_5_A" :: ["A"(0)] -(0)-> "A"(0, 1)
"c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
"c_7_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1)
"c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1, 0)
"c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(0, 1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
cond_eval_expr_2#(Succ(x10),x5) -> c_3(cond_eval_expr_3#(eval#1(x5),x10),eval#1#(x5))
eval#1#(Add(x10,x12)) -> c_7(cond_eval_expr_1#(eval#1(x10),x12),eval#1#(x10))
2. Weak:
WORST_CASE(?,O(n^2))